% RA: Relación 02
% OTTER: 8puzle.in
% Departamento de Ciencias de la Computación e Inteligencia Artificial
%==============================================================================


%==============================================================================
% Enunciado
%==============================================================================

% El 8-puzle es una caja que contiene 8 fichas cuadradas enumeradas del 1 al 8
% y un hueco. Cualquier ficha se puede desplazar en horizontal o vertical hacia
% el hueco. Determinar la secuencia de movimientos que llevan desde el estado
% inicial hasta el estado final indicados en la figura. (La solución ha de ser
% lo más general posible).
%
%               ┏━━━┯━━━┯━━━┓              ┏━━━┯━━━┯━━━┓
%               ┃ 4 │ 3 │ 1 ┃              ┃ 1 │ 2 │ 3 ┃
%               ┠───┼───┼───┨              ┠───┼───┼───┨
%               ┃   │ 8 │ 2 ┃              ┃ 4 │ 5 │ 6 ┃
%               ┠───┼───┼───┨              ┠───┼───┼───┨
%               ┃ 5 │ 7 │ 6 ┃              ┃ 7 │ 8 │   ┃
%               ┗━━━┷━━━┷━━━┛              ┗━━━┷━━━┷━━━┛
%               Estado inicial             Estado  final

% Utilizar OTTER para encontrar una solución al problema.

%==============================================================================
% Formalización
%==============================================================================

% Configuración del sistema

set(para_into).

% Lenguaje del problema

% Constantes:
%   Números naturales, l

% Funciones:
%  f(X) : La ficha con el número X.

% Propiedades:
%  estado(L) :
%    L es una lista que representa las filas de un tablero que se puede
%    alcanzar con pasos del juego. Cada fila se separa de la siguiente por la
%    constante l.

% En la lista que representa las filas del tablero, las casillas ocupadas por
% fichas están representadas por el término 'f(x)' donde 'x' es el número de la
% ficha; el hueco está representado por el número 0; y el valor 'l' sirve como
% separador entre filas consecutivas. De esta forma:
% - Dos casillas consecutivas que no tengan el valor 'l' estarán en la misma
%   fila y, si una de ellas es el hueco, se podría hacer un movimiento
%   horizontal. Aquí es importante el papel del símbolo 'l' para evitar un
%   movimiento entre dos elementos de la lista que estén en filas consecutivas,
%   el último de una de ellas y el primero de la siguiente.
% - Dos casillas separadas por tres elementos de la lista, estarán en la misma
%   columna y, si una de ellas es el hueco, se podrían intercambiar.
% El movimiento, tanto horizontal como vertical

list(usable).
% Movimiento de una ficha hacia la izquierda o derecha.
 [0,f(x)|y] = [f(x),0|y].

% Movimiento de una ficha hacia arriba o abajo.
 [0,x1,x2,x3,f(x)|y] = [f(x),x1,x2,x3,0|y].

% Situación inicial.
 estado([f(4),f(3),f(1),l,
          0,  f(8),f(2),l,
         f(5),f(7),f(6)]).
end_of_list.

list(sos).
% Objetivo final.
 -estado([f(1),f(2),f(3),l,
          f(4),f(5),f(6),l,
          f(7),f(8), 0  ]).
end_of_list.

%==============================================================================
% Soluciones:
%==============================================================================

% Se obtiene la siguiente prueba:

% ---------------- PROOF ----------------
%    1 [] [0,f(x)|y]=[f(x),0|y].
%    2 [] [0,x1,x2,x3,f(x)|y]=[f(x),x1,x2,x3,0|y].
%    3 [] estado([f(4),f(3),f(1),l,0,f(8),f(2),l,f(5),f(7),f(6)]).
%    4 [] -estado([f(1),f(2),f(3),l,f(4),f(5),f(6),l,f(7),f(8),0]).
%    6 [para_into,4.1.1.2.2.2.2.2.2,2.1.2]
%        -estado([f(1),f(2),f(3),l,f(4),f(5),0,l,f(7),f(8),f(6)]).
%   10 [para_into,6.1.1.2.2,2.1.2]
%        -estado([f(1),f(2),0,l,f(4),f(5),f(3),l,f(7),f(8),f(6)]).
%   18 [para_into,10.1.1.2,1.1.2]
%        -estado([f(1),0,f(2),l,f(4),f(5),f(3),l,f(7),f(8),f(6)]).
%   34 [para_into,18.1.1,1.1.2]
%        -estado([0,f(1),f(2),l,f(4),f(5),f(3),l,f(7),f(8),f(6)]).
%   54 [para_into,34.1.1,2.1.1]
%        -estado([f(4),f(1),f(2),l,0,f(5),f(3),l,f(7),f(8),f(6)]).
%   93 [para_into,54.1.1.2.2.2.2,1.1.1]
%        -estado([f(4),f(1),f(2),l,f(5),0,f(3),l,f(7),f(8),f(6)]).
%  154 [para_into,93.1.1.2.2.2.2.2,1.1.1]
%        -estado([f(4),f(1),f(2),l,f(5),f(3),0,l,f(7),f(8),f(6)]).
%  269 [para_into,154.1.1.2.2,2.1.2]
%        -estado([f(4),f(1),0,l,f(5),f(3),f(2),l,f(7),f(8),f(6)]).
%  422 [para_into,269.1.1.2,1.1.2]
%        -estado([f(4),0,f(1),l,f(5),f(3),f(2),l,f(7),f(8),f(6)]).
%  706 [para_into,422.1.1.2,2.1.1]
%        -estado([f(4),f(3),f(1),l,f(5),0,f(2),l,f(7),f(8),f(6)]).
% 1098 [para_into,706.1.1.2.2.2.2.2,2.1.1]
%        -estado([f(4),f(3),f(1),l,f(5),f(8),f(2),l,f(7),0,f(6)]).
% 1840 [para_into,1098.1.1.2.2.2.2.2.2.2.2,1.1.2]
%        -estado([f(4),f(3),f(1),l,f(5),f(8),f(2),l,0,f(7),f(6)]).
% 2865 [para_into,1840.1.1.2.2.2.2,2.1.2]
%        -estado([f(4),f(3),f(1),l,0,f(8),f(2),l,f(5),f(7),f(6)]).
% 2866 [binary,2865.1,3.1] $F.
% ------------ end of proof -------------

%==============================================================================
